Termination proof of /tmp/tmpb4ch

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇒)

↳2 JBCTerminationGraph

↳3 FIGtoITRSProof (⇒)

↳4 AND

    ↳5 IDP

        ↳6 IDPtoQDPProof (⇒)

        ↳7 QDP

        ↳8 UsableRulesProof (⇔)

        ↳9 QDP

        ↳10 QReductionProof (⇔)

        ↳11 QDP

        ↳12 UsableRulesReductionPairsProof (⇔)

        ↳13 QDP

        ↳14 PisEmptyProof (⇔)

        ↳15 YES

    ↳16 IDP

        ↳17 IDPtoQDPProof (⇒)

        ↳18 QDP

        ↳19 UsableRulesProof (⇔)

        ↳20 QDP

        ↳21 QReductionProof (⇔)

        ↳22 QDP

        ↳23 Rewriting (⇔)

        ↳24 QDP

        ↳25 UsableRulesProof (⇔)

        ↳26 QDP

        ↳27 QReductionProof (⇔)

        ↳28 QDP

        ↳29 QDPOrderProof (⇔)

        ↳30 QDP

        ↳31 DependencyGraphProof (⇔)

        ↳32 TRUE

    ↳33 IDP

        ↳34 IDPNonInfProof (⇒)

        ↳35 AND

            ↳36 IDP

                ↳37 IDependencyGraphProof (⇔)

                ↳38 TRUE

            ↳39 IDP

                ↳40 IDependencyGraphProof (⇔)

                ↳41 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_14 (Sun Microsystems Inc.) Main-Class: Count

public class Count {

  public static int count(Tree x) {
    // counts the number of inner nodes in the tree x

    if (x == null) return 0;
    if (x.l == null) return 1 + count(x.r);
    else return count(Flatten.flatten(x));
  }

  public static void main(String[] args) {
    Random.args = args;

    Tree x = Tree.createTree();
    Tree y = Flatten.flatten(x);
    count(x);
  }
}


public class Flatten {

  public static Tree flatten(Tree x) {

    if (x == null) return null;
    if (x.l == null) return new Tree(null, flatten(x.r));
    else return flatten(new Tree(x.l.l, new Tree(x.l.r, x.r)));
  }

  public static void main(String[] args) {
    Random.args = args;
    Tree x = Tree.createTree();
    Tree y = flatten(x);
  }
}




public class Random {
    static String[] args;
    static int index = 0;

    public static int random() {
        if (args.length <= index) {
            return 0;
        }
        final String string = args[index];
        index++;
        if (string == null) {
            return 0;
        }
        return string.length();
    }
}


public class Tree {
    Tree l;
    Tree r;
    int value;

    public Tree(final Tree l, final Tree r) {
        this.l = l;
        this.r = r;
    }

    public Tree() {
    }

    public static Tree createNode() {
        final Tree result = new Tree();
        result.value = Random.random();
        return result;
    }

    public static Tree createTree() {
        int counter = Random.random();
        if (counter == 0) {
            return null;
        }
        final Tree result = createNode();
        Tree t = result;

        while (counter > 0) {
            final int branch = Random.random();
            if (branch > 0) {
                if (t.l == null) {
                    t.l = createNode();
                    t = result;
                } else {
                    t = t.l;
                }
            } else {
                if (t.r == null) {
                    t.r = createNode();
                    t = result;
                } else {
                    t = t.r;
                }
            }
            counter--;
        }

        return result;
    }

    public static void main(final String[] args) {
        Random.args = args;
        createTree();
    }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Count.main([Ljava/lang/String;)V: Graph of 123 nodes with 0 SCCs.

Tree.createTree()LTree;: Graph of 346 nodes with 1 SCC.

Flatten.flatten(LTree;)LTree;: Graph of 113 nodes with 0 SCCs.

Count.count(LTree;)I: Graph of 57 nodes with 0 SCCs.

Tree.createNode()LTree;: Graph of 99 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 56 rules for P and 59 rules for R.

Combined rules. Obtained 2 rules for P and 11 rules for R.

Filtered ground terms:

2313_1_flatten_InvokeMethod(x1, x2, x3, x4, x5, x6) → 2313_1_flatten_InvokeMethod(x1, x2, x6)
Tree(x1, x2, x3) → Tree(x2, x3)
2005_0_flatten_NONNULL(x1, x2, x3) → 2005_0_flatten_NONNULL(x2, x3)
5483_0_flatten_Return(x1, x2, x3) → 5483_0_flatten_Return(x2, x3)
5681_0_flatten_Return(x1, x2) → 5681_0_flatten_Return(x2)
3788_0_flatten_Return(x1, x2, x3) → 3788_0_flatten_Return(x2, x3)
4141_0_flatten_Return(x1, x2) → 4141_0_flatten_Return(x2)
2520_0_flatten_Return(x1, x2, x3) → 2520_0_flatten_Return
2067_0_flatten_Return(x1, x2, x3) → 2067_0_flatten_Return

Filtered duplicate args:

2005_0_flatten_NONNULL(x1, x2) → 2005_0_flatten_NONNULL(x2)

Finished conversion. Obtained 2 rules for P and 11 rules for R. System has no predefined symbols.

Log for SCC 1:

Generated 28 rules for P and 147 rules for R.

Combined rules. Obtained 4 rules for P and 27 rules for R.

Filtered ground terms:

Tree(x1, x2, x3) → Tree(x2, x3)
3130_0_count_NONNULL(x1, x2, x3) → 3130_0_count_NONNULL(x2, x3)
5681_0_flatten_Return(x1, x2) → 5681_0_flatten_Return(x2)
4141_0_flatten_Return(x1, x2) → 4141_0_flatten_Return(x2)
3551_0_flatten_Load(x1, x2) → 3551_0_flatten_Load(x2)
3606_0_flatten_Return(x1, x2, x3) → 3606_0_flatten_Return
3599_0_flatten_Load(x1, x2) → 3599_0_flatten_Load(x2)
3604_0_flatten_Return(x1, x2, x3) → 3604_0_flatten_Return
5483_0_flatten_Return(x1, x2, x3) → 5483_0_flatten_Return(x2, x3)
3788_0_flatten_Return(x1, x2, x3) → 3788_0_flatten_Return(x2, x3)
2005_0_flatten_NONNULL(x1, x2, x3) → 2005_0_flatten_NONNULL(x2, x3)
2520_0_flatten_Return(x1, x2, x3) → 2520_0_flatten_Return
2313_1_flatten_InvokeMethod(x1, x2, x3, x4, x5, x6) → 2313_1_flatten_InvokeMethod(x1, x2, x6)
2067_0_flatten_Return(x1, x2, x3) → 2067_0_flatten_Return
4178_0_count_Return(x1, x2) → 4178_0_count_Return(x2)
4800_0_count_Return(x1, x2) → 4800_0_count_Return(x2)
4370_0_count_Return(x1) → 4370_0_count_Return
3638_0_count_Return(x1, x2) → 3638_0_count_Return
2951_0_count_Return(x1, x2) → 2951_0_count_Return
5588_0_flatten_Return(x1, x2, x3) → 5588_0_flatten_Return(x2, x3)
3839_0_flatten_Return(x1, x2, x3) → 3839_0_flatten_Return(x2, x3)
3557_0_flatten_Return(x1, x2, x3) → 3557_0_flatten_Return
3555_0_flatten_Return(x1, x2, x3) → 3555_0_flatten_Return

Filtered duplicate args:

2005_0_flatten_NONNULL(x1, x2) → 2005_0_flatten_NONNULL(x2)

Filtered all free variables:

3839_0_flatten_Return(x1, x2) → 3839_0_flatten_Return(x1)
5588_0_flatten_Return(x1, x2) → 5588_0_flatten_Return(x1)

Finished conversion. Obtained 4 rules for P and 27 rules for R. System has no predefined symbols.

Log for SCC 2:

Generated 204 rules for P and 195 rules for R.

Combined rules. Obtained 37 rules for P and 34 rules for R.

Filtered ground terms:

10533_0_createTree_FieldAccess(x1, x2, x3, x4, x5) → 10533_0_createTree_FieldAccess(x2, x3, x4, x5)
Tree(x1, x2, x3) → Tree(x2, x3)
10302_0_random_GT(x1, x2, x3) → 10302_0_random_GT(x2, x3)
10598_0_random_IntArithmetic(x1, x2, x3, x4) → 10598_0_random_IntArithmetic(x2, x3)
10199_0_createTree_LE(x1, x2, x3, x4, x5) → 10199_0_createTree_LE(x2, x3, x4, x5)
Cond_12816_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_12816_1_createTree_InvokeMethod1(x1, x3, x4, x5)
1963_0_createNode_Return(x1, x2) → 1963_0_createNode_Return
Cond_12816_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_12816_1_createTree_InvokeMethod(x1, x3, x4, x5)
1642_0_createNode_Return(x1, x2) → 1642_0_createNode_Return
12816_0_createNode_New(x1) → 12816_0_createNode_New
Cond_12928_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_12928_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_12928_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_12928_1_createTree_InvokeMethod(x1, x3, x4, x5)
12928_0_createNode_New(x1) → 12928_0_createNode_New
Cond_12782_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_12782_1_createTree_InvokeMethod1(x1, x3)
12782_1_createTree_InvokeMethod(x1, x2, x3, x4) → 12782_1_createTree_InvokeMethod(x1, x2)
Cond_12782_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_12782_1_createTree_InvokeMethod(x1, x3)
12782_0_createNode_New(x1) → 12782_0_createNode_New
Cond_10598_1_createTree_InvokeMethod3(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod3(x1, x2, x3)
Cond_13012_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_13012_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_13012_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_13012_1_createTree_InvokeMethod(x1, x3, x4, x5)
13012_0_createNode_New(x1) → 13012_0_createNode_New
Cond_11081_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_11081_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_11081_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_11081_1_createTree_InvokeMethod(x1, x3, x4, x5)
11081_0_createNode_New(x1) → 11081_0_createNode_New
Cond_10533_0_createTree_FieldAccess2(x1, x2, x3, x4, x5, x6) → Cond_10533_0_createTree_FieldAccess2(x1, x3, x4, x5, x6)
Cond_11280_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_11280_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_11280_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_11280_1_createTree_InvokeMethod(x1, x3, x4, x5)
11280_0_createNode_New(x1) → 11280_0_createNode_New
Cond_10533_0_createTree_FieldAccess1(x1, x2, x3, x4, x5, x6) → Cond_10533_0_createTree_FieldAccess1(x1, x3, x4, x5, x6)
Cond_11044_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_11044_1_createTree_InvokeMethod1(x1, x3)
11044_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11044_1_createTree_InvokeMethod(x1, x2)
Cond_11044_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_11044_1_createTree_InvokeMethod(x1, x3)
11044_0_createNode_New(x1) → 11044_0_createNode_New
Cond_11456_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_11456_1_createTree_InvokeMethod1(x1, x3, x4, x5)
Cond_11456_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_11456_1_createTree_InvokeMethod(x1, x3, x4, x5)
11456_0_createNode_New(x1) → 11456_0_createNode_New
Cond_10533_0_createTree_FieldAccess(x1, x2, x3, x4, x5, x6) → Cond_10533_0_createTree_FieldAccess(x1, x3, x4, x5, x6)
10436_0_random_ArrayAccess(x1, x2, x3) → 10436_0_random_ArrayAccess(x2, x3)
10297_0_random_GT(x1, x2, x3) → 10297_0_random_GT(x2, x3)
Cond_10199_0_createTree_LE1(x1, x2, x3, x4, x5, x6) → Cond_10199_0_createTree_LE1(x1, x3, x4, x5, x6)
Cond_10199_0_createTree_LE(x1, x2, x3, x4, x5, x6) → Cond_10199_0_createTree_LE(x1, x3, x4, x5, x6)
2056_0_createNode_InvokeMethod(x1, x2, x3, x4) → 2056_0_createNode_InvokeMethod
java.lang.ArrayIndexOutOfBoundsException(x1) → java.lang.ArrayIndexOutOfBoundsException
java.lang.IndexOutOfBoundsException(x1) → java.lang.IndexOutOfBoundsException
java.lang.RuntimeException(x1) → java.lang.RuntimeException
java.lang.Exception(x1) → java.lang.Exception
java.lang.Throwable(x1) → java.lang.Throwable
Cond_1611_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_1611_1_createNode_InvokeMethod(x1, x2)
1611_0_random_ArrayAccess(x1, x2, x3) → 1611_0_random_ArrayAccess(x2, x3)
1611_1_createNode_InvokeMethod(x1, x2, x3) → 1611_1_createNode_InvokeMethod(x1)
Cond_1700_1_createNode_InvokeMethod1(x1, x2, x3, x4) → Cond_1700_1_createNode_InvokeMethod1(x1, x2)
1700_0_random_IntArithmetic(x1, x2, x3, x4) → 1700_0_random_IntArithmetic(x2, x3)
1700_1_createNode_InvokeMethod(x1, x2, x3) → 1700_1_createNode_InvokeMethod(x1)
Cond_1700_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_1700_1_createNode_InvokeMethod(x1, x2)
Cond_1639_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_1639_1_createNode_InvokeMethod(x1, x2)
1639_0_random_ArrayAccess(x1, x2, x3) → 1639_0_random_ArrayAccess(x2, x3)
1639_1_createNode_InvokeMethod(x1, x2, x3) → 1639_1_createNode_InvokeMethod(x1)
2088_0_createNode_InvokeMethod(x1, x2, x3, x4) → 2088_0_createNode_InvokeMethod
Cond_1640_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_1640_1_createNode_InvokeMethod(x1, x2)
1640_0_random_ArrayAccess(x1, x2, x3) → 1640_0_random_ArrayAccess(x2, x3)
1640_1_createNode_InvokeMethod(x1, x2, x3) → 1640_1_createNode_InvokeMethod(x1)
Cond_1521_1_createNode_InvokeMethod3(x1, x2, x3, x4) → Cond_1521_1_createNode_InvokeMethod3(x1, x2)
1521_0_random_GT(x1, x2, x3) → 1521_0_random_GT(x2, x3)
1521_1_createNode_InvokeMethod(x1, x2, x3) → 1521_1_createNode_InvokeMethod(x1)
Cond_1521_1_createNode_InvokeMethod2(x1, x2, x3, x4) → Cond_1521_1_createNode_InvokeMethod2(x1, x2)
Cond_1521_1_createNode_InvokeMethod1(x1, x2, x3, x4) → Cond_1521_1_createNode_InvokeMethod1(x1, x2)
Cond_1521_1_createNode_InvokeMethod(x1, x2, x3, x4) → Cond_1521_1_createNode_InvokeMethod(x1, x2)
12976_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 12976_0_createTree_InvokeMethod(x3, x4, x5)
13109_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 13109_0_createTree_InvokeMethod(x3, x4, x5)
12923_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 12923_0_createTree_InvokeMethod(x3)
13204_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 13204_0_createTree_InvokeMethod(x3, x4, x5)
11354_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11354_0_createTree_InvokeMethod(x3, x4, x5)
11584_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11584_0_createTree_InvokeMethod(x3, x4, x5)
11275_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11275_0_createTree_InvokeMethod(x3)
11724_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11724_0_createTree_InvokeMethod(x3, x4, x5)
10224_0_createTree_Return(x1, x2) → 10224_0_createTree_Return(x2)
12836_0_createNode_InvokeMethod(x1, x2, x3, x4) → 12836_0_createNode_InvokeMethod
12951_0_createNode_InvokeMethod(x1, x2, x3, x4) → 12951_0_createNode_InvokeMethod
12798_0_createNode_InvokeMethod(x1, x2, x3, x4) → 12798_0_createNode_InvokeMethod
13058_0_createNode_InvokeMethod(x1, x2, x3, x4) → 13058_0_createNode_InvokeMethod

Filtered duplicate args:

10533_0_createTree_FieldAccess(x1, x2, x3, x4) → 10533_0_createTree_FieldAccess(x1, x2, x4)
10199_0_createTree_LE(x1, x2, x3, x4) → 10199_0_createTree_LE(x2, x3, x4)
Cond_10533_0_createTree_FieldAccess2(x1, x2, x3, x4, x5) → Cond_10533_0_createTree_FieldAccess2(x1, x2, x3, x5)
Cond_10533_0_createTree_FieldAccess1(x1, x2, x3, x4, x5) → Cond_10533_0_createTree_FieldAccess1(x1, x2, x3, x5)
Cond_10533_0_createTree_FieldAccess(x1, x2, x3, x4, x5) → Cond_10533_0_createTree_FieldAccess(x1, x2, x3, x5)
Cond_10199_0_createTree_LE1(x1, x2, x3, x4, x5) → Cond_10199_0_createTree_LE1(x1, x3, x4, x5)
Cond_10199_0_createTree_LE(x1, x2, x3, x4, x5) → Cond_10199_0_createTree_LE(x1, x3, x4, x5)

Filtered all non-integer terms:

10199_0_createTree_LE(x1, x2, x3) → 10199_0_createTree_LE(x3)
Cond_10199_0_createTree_LE(x1, x2, x3, x4) → Cond_10199_0_createTree_LE(x1, x4)
10297_1_createTree_InvokeMethod(x1, x2, x3, x4) → 10297_1_createTree_InvokeMethod(x1, x2)
Cond_10199_0_createTree_LE1(x1, x2, x3, x4) → Cond_10199_0_createTree_LE1(x1, x4)
10302_1_createTree_InvokeMethod(x1, x2, x3, x4) → 10302_1_createTree_InvokeMethod(x1, x2)
Cond_10297_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_10297_1_createTree_InvokeMethod(x1, x2, x3)
10436_1_createTree_InvokeMethod(x1, x2, x3, x4) → 10436_1_createTree_InvokeMethod(x1, x2)
Cond_10436_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_10436_1_createTree_InvokeMethod(x1, x2, x3)
10598_1_createTree_InvokeMethod(x1, x2, x3, x4) → 10598_1_createTree_InvokeMethod(x1, x2)
10598_0_random_IntArithmetic(x1, x2) → 10598_0_random_IntArithmetic(x2)
Cond_10598_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod(x1, x2, x3)
10533_0_createTree_FieldAccess(x1, x2, x3) → 10533_0_createTree_FieldAccess(x1)
Tree(x1, x2) → Tree
Cond_10533_0_createTree_FieldAccess(x1, x2, x3, x4) → Cond_10533_0_createTree_FieldAccess(x1, x2)
11456_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11456_1_createTree_InvokeMethod(x1, x2)
Cond_11456_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_11456_1_createTree_InvokeMethod(x1, x2)
Cond_11456_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_11456_1_createTree_InvokeMethod1(x1, x2)
Cond_10533_0_createTree_FieldAccess1(x1, x2, x3, x4) → Cond_10533_0_createTree_FieldAccess1(x1, x2)
11280_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11280_1_createTree_InvokeMethod(x1, x2)
Cond_11280_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_11280_1_createTree_InvokeMethod(x1, x2)
Cond_11280_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_11280_1_createTree_InvokeMethod1(x1, x2)
Cond_10533_0_createTree_FieldAccess2(x1, x2, x3, x4) → Cond_10533_0_createTree_FieldAccess2(x1, x2)
11081_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11081_1_createTree_InvokeMethod(x1, x2)
Cond_11081_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_11081_1_createTree_InvokeMethod(x1, x2)
Cond_11081_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_11081_1_createTree_InvokeMethod1(x1, x2)
Cond_10598_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod1(x1, x2, x3)
Cond_10598_1_createTree_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod2(x1, x2, x3)
13012_1_createTree_InvokeMethod(x1, x2, x3, x4) → 13012_1_createTree_InvokeMethod(x1, x2)
Cond_13012_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_13012_1_createTree_InvokeMethod(x1, x2)
Cond_13012_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_13012_1_createTree_InvokeMethod1(x1, x2)
Cond_10598_1_createTree_InvokeMethod4(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod4(x1, x2, x3)
Cond_10598_1_createTree_InvokeMethod5(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod5(x1, x2, x3)
12928_1_createTree_InvokeMethod(x1, x2, x3, x4) → 12928_1_createTree_InvokeMethod(x1, x2)
Cond_12928_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_12928_1_createTree_InvokeMethod(x1, x2)
Cond_12928_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_12928_1_createTree_InvokeMethod1(x1, x2)
Cond_10598_1_createTree_InvokeMethod6(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod6(x1, x2, x3)
Cond_10598_1_createTree_InvokeMethod7(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod7(x1, x2, x3)
12816_1_createTree_InvokeMethod(x1, x2, x3, x4) → 12816_1_createTree_InvokeMethod(x1, x2)
Cond_12816_1_createTree_InvokeMethod(x1, x2, x3, x4) → Cond_12816_1_createTree_InvokeMethod(x1, x2)
Cond_12816_1_createTree_InvokeMethod1(x1, x2, x3, x4) → Cond_12816_1_createTree_InvokeMethod1(x1, x2)
Cond_10598_1_createTree_InvokeMethod8(x1, x2, x3, x4, x5) → Cond_10598_1_createTree_InvokeMethod8(x1, x2, x3)
Cond_10302_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_10302_1_createTree_InvokeMethod(x1, x2, x3)
10224_0_createTree_Return(x1) → 10224_0_createTree_Return
11724_0_createTree_InvokeMethod(x1, x2, x3) → 11724_0_createTree_InvokeMethod(x1)
11584_0_createTree_InvokeMethod(x1, x2, x3) → 11584_0_createTree_InvokeMethod(x1)
11354_0_createTree_InvokeMethod(x1, x2, x3) → 11354_0_createTree_InvokeMethod(x1)
13204_0_createTree_InvokeMethod(x1, x2, x3) → 13204_0_createTree_InvokeMethod(x1)
13109_0_createTree_InvokeMethod(x1, x2, x3) → 13109_0_createTree_InvokeMethod(x1)
12976_0_createTree_InvokeMethod(x1, x2, x3) → 12976_0_createTree_InvokeMethod(x1)
1700_0_random_IntArithmetic(x1, x2) → 1700_0_random_IntArithmetic(x2)

Filtered all free variables:

10297_1_createTree_InvokeMethod(x1, x2) → 10297_1_createTree_InvokeMethod(x2)
10302_1_createTree_InvokeMethod(x1, x2) → 10302_1_createTree_InvokeMethod(x2)
Cond_10297_1_createTree_InvokeMethod(x1, x2, x3) → Cond_10297_1_createTree_InvokeMethod(x1, x3)
10436_1_createTree_InvokeMethod(x1, x2) → 10436_1_createTree_InvokeMethod(x2)
Cond_10436_1_createTree_InvokeMethod(x1, x2, x3) → Cond_10436_1_createTree_InvokeMethod(x1, x3)
10598_1_createTree_InvokeMethod(x1, x2) → 10598_1_createTree_InvokeMethod(x2)
Cond_10598_1_createTree_InvokeMethod(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod(x1, x3)
Cond_10598_1_createTree_InvokeMethod1(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod1(x1, x3)
Cond_10598_1_createTree_InvokeMethod2(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod2(x1, x3)
Cond_10598_1_createTree_InvokeMethod3(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod3(x1, x3)
Cond_10598_1_createTree_InvokeMethod4(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod4(x1, x3)
Cond_10598_1_createTree_InvokeMethod5(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod5(x1, x3)
Cond_10598_1_createTree_InvokeMethod6(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod6(x1, x3)
Cond_10598_1_createTree_InvokeMethod7(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod7(x1, x3)
Cond_10598_1_createTree_InvokeMethod8(x1, x2, x3) → Cond_10598_1_createTree_InvokeMethod8(x1, x3)
Cond_10302_1_createTree_InvokeMethod(x1, x2, x3) → Cond_10302_1_createTree_InvokeMethod(x1, x3)
1521_0_random_GT(x1, x2) → 1521_0_random_GT
1611_0_random_ArrayAccess(x1, x2) → 1611_0_random_ArrayAccess(x1)
ARRAY(x1, x2) → ARRAY(x1)
1639_0_random_ArrayAccess(x1, x2) → 1639_0_random_ArrayAccess(x1)
1640_0_random_ArrayAccess(x1, x2) → 1640_0_random_ArrayAccess(x1)
1700_0_random_IntArithmetic(x1) → 1700_0_random_IntArithmetic

Filtered ground terms:

Cond_1700_1_createNode_InvokeMethod1(x1, x2) → Cond_1700_1_createNode_InvokeMethod1(x1)
1700_1_createNode_InvokeMethod(x1) → 1700_1_createNode_InvokeMethod
Cond_1700_1_createNode_InvokeMethod(x1, x2) → Cond_1700_1_createNode_InvokeMethod(x1)
Cond_1521_1_createNode_InvokeMethod3(x1, x2) → Cond_1521_1_createNode_InvokeMethod3(x1)
1521_1_createNode_InvokeMethod(x1) → 1521_1_createNode_InvokeMethod
Cond_1521_1_createNode_InvokeMethod2(x1, x2) → Cond_1521_1_createNode_InvokeMethod2(x1)
Cond_1521_1_createNode_InvokeMethod1(x1, x2) → Cond_1521_1_createNode_InvokeMethod1(x1)
Cond_1521_1_createNode_InvokeMethod(x1, x2) → Cond_1521_1_createNode_InvokeMethod(x1)

Combined rules. Obtained 25 rules for P and 29 rules for R.

Finished conversion. Obtained 25 rules for P and 29 rules for R. System has predefined symbols.

(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))

The integer pair graph contains the following rules and edges:
(0): 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))) → 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))))
(1): 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(NULL, x0[1]))) → 2005_0_FLATTEN_NONNULL(x0[1])

(0) -> (0), if ((java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))) →^* java.lang.Object(Tree(java.lang.Object(Tree(x0[0]', x1[0]')), x2[0]'))))

(0) -> (1), if ((java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))) →^* java.lang.Object(Tree(NULL, x0[1]))))

(1) -> (0), if ((x0[1] →^* java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))))

(1) -> (1), if ((x0[1] →^* java.lang.Object(Tree(NULL, x0[1]'))))

The set Q consists of the following terms:
2005_0_flatten_NONNULL(NULL)
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))

(6) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))) → 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))))
2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(NULL, x0[1]))) → 2005_0_FLATTEN_NONNULL(x0[1])

The TRS R consists of the following rules:

2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))

The set Q consists of the following terms:

2005_0_flatten_NONNULL(NULL)
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))) → 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))))
2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(NULL, x0[1]))) → 2005_0_FLATTEN_NONNULL(x0[1])

R is empty.
The set Q consists of the following terms:

2005_0_flatten_NONNULL(NULL)
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))

We have to consider all minimal (P,Q,R)-chains.

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

2005_0_flatten_NONNULL(NULL)
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))) → 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))))
2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(NULL, x0[1]))) → 2005_0_FLATTEN_NONNULL(x0[1])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0[0], x1[0])), x2[0]))) → 2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(x0[0], java.lang.Object(Tree(x1[0], x2[0])))))
2005_0_FLATTEN_NONNULL(java.lang.Object(Tree(NULL, x0[1]))) → 2005_0_FLATTEN_NONNULL(x0[1])

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(2005_0_FLATTEN_NONNULL(x₁)) = 2·x₁
POL(NULL) = 0
POL(Tree(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(java.lang.Object(x₁)) = 1 + x₁

(13) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(15) YES

(16) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
3551_0_flatten_Load(NULL) → 3555_0_flatten_Return
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL))) → 3557_0_flatten_Return
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, o730))))) → 3839_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, o730)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(o1125, o1126)), o1127))))) → 5588_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(o1125, o1126)), o1127)))))
4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 4370_0_count_Return
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0), x1)))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 3638_0_count_Return
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))))
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_0_flatten_Load(NULL) → 3604_0_flatten_Return
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL))) → 3606_0_flatten_Return

The integer pair graph contains the following rules and edges:
(0): 3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
(1): 3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
(2): 3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
(3): 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])

(0) -> (1), if ((3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) →^* 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))))∧(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])) →^* java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))))

(0) -> (2), if ((3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) →^* 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))))∧(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])) →^* java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))))

(1) -> (0), if ((java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))) →^* java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))∧(NULL →^* java.lang.Object(x0[0])))

(1) -> (3), if (java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))) →^* java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))))

(2) -> (0), if ((java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))) →^* java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))∧(NULL →^* java.lang.Object(x0[0])))

(2) -> (3), if (java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))) →^* java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))))

(3) -> (0), if ((java.lang.Object(Tree(x0[3], x1[3])) →^* java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))∧(x0[3] →^* java.lang.Object(x0[0])))

(3) -> (3), if ((java.lang.Object(Tree(x0[3], x1[3])) →^* java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3]', x1[3]')))))∧(x0[3] →^* NULL))

The set Q consists of the following terms:
3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

(17) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])

The TRS R consists of the following rules:

3551_0_flatten_Load(NULL) → 3555_0_flatten_Return
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL))) → 3557_0_flatten_Return
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, o730))))) → 3839_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, o730)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(o1125, o1126)), o1127))))) → 5588_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(o1125, o1126)), o1127)))))
4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 4370_0_count_Return
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0), x1)))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 3638_0_count_Return
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))))
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_0_flatten_Load(NULL) → 3604_0_flatten_Return
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL))) → 3606_0_flatten_Return

The set Q consists of the following terms:

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(19) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])

The TRS R consists of the following rules:

3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(21) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

4183_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3607_1_count_InvokeMethod(2951_0_count_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
3607_1_count_InvokeMethod(3638_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
3607_1_count_InvokeMethod(4178_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3607_1_count_InvokeMethod(4370_0_count_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3607_1_count_InvokeMethod(4800_0_count_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])

The TRS R consists of the following rules:

3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(23) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule 3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) at position [0] we obtained the following new rules [LPAR04]:

3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])
3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(25) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])
3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))
2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(27) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

3551_0_flatten_Load(NULL)
3551_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3551_0_flatten_Load(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3551_0_flatten_Load(java.lang.Object(Tree(java.lang.Object(x0), x1)))

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])
3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(x0[3], x1[3])))), NULL) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(x0[3], x1[3])), x0[3])

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(2005_0_flatten_NONNULL(x₁)) = x₁
POL(2067_0_flatten_Return) = 0
POL(2313_1_flatten_InvokeMethod(x₁, x₂, x₃)) = 1 + x₁
POL(2520_0_flatten_Return) = 1
POL(3130_0_COUNT_NONNULL(x₁, x₂)) = x₁
POL(3551_1_COUNT_INVOKEMETHOD(x₁, x₂)) = x₁
POL(3599_0_flatten_Load(x₁)) = x₁
POL(3599_1_flatten_InvokeMethod(x₁, x₂)) = x₁
POL(3788_0_flatten_Return(x₁, x₂)) = x₂
POL(4141_0_flatten_Return(x₁)) = x₁
POL(5483_0_flatten_Return(x₁, x₂)) = x₂
POL(5681_0_flatten_Return(x₁)) = x₁
POL(NULL) = 0
POL(Tree(x₁, x₂)) = x₁ + x₂
POL(java.lang.Object(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented:

2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

3551_1_COUNT_INVOKEMETHOD(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1]))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1[1], x2[1])), x3[1])), x4[1]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[1])))), NULL)
3551_1_COUNT_INVOKEMETHOD(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2]))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1[2])), x2[2]))) → 3130_0_COUNT_NONNULL(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0[2])))), NULL)
3130_0_COUNT_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])), java.lang.Object(x0[0])) → 3551_1_COUNT_INVOKEMETHOD(2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 3599_1_flatten_InvokeMethod(3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))), java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2))))) → 2005_0_flatten_NONNULL(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3))))) → 4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0))) → 2313_1_flatten_InvokeMethod(2005_0_flatten_NONNULL(x0), java.lang.Object(Tree(NULL, x0)), x0)
2005_0_flatten_NONNULL(NULL) → 2067_0_flatten_Return
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2))) → 5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1)))))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))))) → 3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3)))))))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL) → 2520_0_flatten_Return

The set Q consists of the following terms:

2005_0_flatten_NONNULL(NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(NULL, x0)))
2313_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), x4)))
2313_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), x2)))
2313_1_flatten_InvokeMethod(2520_0_flatten_Return, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, NULL)))), java.lang.Object(Tree(NULL, NULL)))
2313_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
2313_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
2313_1_flatten_InvokeMethod(2067_0_flatten_Return, java.lang.Object(Tree(NULL, NULL)), NULL)
2005_0_flatten_NONNULL(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
3599_0_flatten_Load(java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
3599_1_flatten_InvokeMethod(3788_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x1))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0)))))
3599_1_flatten_InvokeMethod(5483_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x3))))))), java.lang.Object(Tree(NULL, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))))
3599_1_flatten_InvokeMethod(4141_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)), java.lang.Object(Tree(x4, x5)))))
3599_1_flatten_InvokeMethod(5681_0_flatten_Return(java.lang.Object(Tree(NULL, java.lang.Object(Tree(NULL, x0))))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(x2, x3)))))
3599_0_flatten_Load(NULL)
3599_0_flatten_Load(java.lang.Object(Tree(NULL, NULL)))

We have to consider all minimal (P,Q,R)-chains.

(31) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(32) TRUE

(33) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
11456_0_createNode_New → 13058_0_createNode_InvokeMethod
11456_0_createNode_New → 12798_0_createNode_InvokeMethod
11456_0_createNode_New → 12951_0_createNode_InvokeMethod
11456_0_createNode_New → 12836_0_createNode_InvokeMethod
10199_0_createTree_LE(0) → 10224_0_createTree_Return
11456_0_createNode_New → 1521_1_createNode_InvokeMethod
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11724_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11724_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11275_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11275_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11584_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11584_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11354_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11354_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 13204_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 12923_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 13109_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 12976_0_createTree_InvokeMethod(x0)
1521_1_createNode_InvokeMethod → 1642_0_createNode_Return
1521_1_createNode_InvokeMethod → 2056_0_createNode_InvokeMethod
1521_1_createNode_InvokeMethod → 2088_0_createNode_InvokeMethod
1521_1_createNode_InvokeMethod → 1963_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0]) → COND_11456_1_CREATETREE_INVOKEMETHOD(x0[0] > 0, 1642_0_createNode_Return, x0[0])
(1): COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1]) → 10199_0_CREATETREE_LE(x0[1] + -1)
(2): 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2]) → COND_11456_1_CREATETREE_INVOKEMETHOD1(x0[2] > 0, 1963_0_createNode_Return, x0[2])
(3): COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3]) → 10199_0_CREATETREE_LE(x0[3] + -1)
(4): 10199_0_CREATETREE_LE(x0[4]) → COND_10199_0_CREATETREE_LE(x0[4] > 0, x0[4])
(5): COND_10199_0_CREATETREE_LE(TRUE, x0[5]) → 10199_0_CREATETREE_LE(x0[5] + -1)
(6): 10199_0_CREATETREE_LE(x0[6]) → COND_10199_0_CREATETREE_LE1(x0[6] > 0, x0[6])
(7): COND_10199_0_CREATETREE_LE1(TRUE, x0[7]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])
(8): 10199_0_CREATETREE_LE(x0[8]) → COND_10199_0_CREATETREE_LE2(x0[8] > 0, x0[8])
(9): COND_10199_0_CREATETREE_LE2(TRUE, x0[9]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])
(10): 10199_0_CREATETREE_LE(x0[10]) → COND_10199_0_CREATETREE_LE3(x0[10] > 0, x0[10])
(11): COND_10199_0_CREATETREE_LE3(TRUE, x0[11]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])
(12): 10199_0_CREATETREE_LE(x0[12]) → COND_10199_0_CREATETREE_LE4(x0[12] > 0, x0[12])
(13): COND_10199_0_CREATETREE_LE4(TRUE, x0[13]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])
(14): 10199_0_CREATETREE_LE(x0[14]) → COND_10199_0_CREATETREE_LE5(x0[14] > 0, x0[14])
(15): COND_10199_0_CREATETREE_LE5(TRUE, x0[15]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])
(16): 10199_0_CREATETREE_LE(x0[16]) → COND_10199_0_CREATETREE_LE6(x0[16] > 0, x0[16])
(17): COND_10199_0_CREATETREE_LE6(TRUE, x0[17]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])
(18): 10199_0_CREATETREE_LE(x0[18]) → COND_10199_0_CREATETREE_LE7(x0[18] > 0, x0[18])
(19): COND_10199_0_CREATETREE_LE7(TRUE, x0[19]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])
(20): 10199_0_CREATETREE_LE(x0[20]) → COND_10199_0_CREATETREE_LE8(x0[20] > 0, x0[20])
(21): COND_10199_0_CREATETREE_LE8(TRUE, x0[21]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])

(0) -> (1), if ((x0[0] > 0 →^* TRUE)∧(x0[0] →^* x0[1]))

(1) -> (4), if ((x0[1] + -1 →^* x0[4]))

(1) -> (6), if ((x0[1] + -1 →^* x0[6]))

(1) -> (8), if ((x0[1] + -1 →^* x0[8]))

(1) -> (10), if ((x0[1] + -1 →^* x0[10]))

(1) -> (12), if ((x0[1] + -1 →^* x0[12]))

(1) -> (14), if ((x0[1] + -1 →^* x0[14]))

(1) -> (16), if ((x0[1] + -1 →^* x0[16]))

(1) -> (18), if ((x0[1] + -1 →^* x0[18]))

(1) -> (20), if ((x0[1] + -1 →^* x0[20]))

(2) -> (3), if ((x0[2] > 0 →^* TRUE)∧(x0[2] →^* x0[3]))

(3) -> (4), if ((x0[3] + -1 →^* x0[4]))

(3) -> (6), if ((x0[3] + -1 →^* x0[6]))

(3) -> (8), if ((x0[3] + -1 →^* x0[8]))

(3) -> (10), if ((x0[3] + -1 →^* x0[10]))

(3) -> (12), if ((x0[3] + -1 →^* x0[12]))

(3) -> (14), if ((x0[3] + -1 →^* x0[14]))

(3) -> (16), if ((x0[3] + -1 →^* x0[16]))

(3) -> (18), if ((x0[3] + -1 →^* x0[18]))

(3) -> (20), if ((x0[3] + -1 →^* x0[20]))

(4) -> (5), if ((x0[4] > 0 →^* TRUE)∧(x0[4] →^* x0[5]))

(5) -> (4), if ((x0[5] + -1 →^* x0[4]))

(5) -> (6), if ((x0[5] + -1 →^* x0[6]))

(5) -> (8), if ((x0[5] + -1 →^* x0[8]))

(5) -> (10), if ((x0[5] + -1 →^* x0[10]))

(5) -> (12), if ((x0[5] + -1 →^* x0[12]))

(5) -> (14), if ((x0[5] + -1 →^* x0[14]))

(5) -> (16), if ((x0[5] + -1 →^* x0[16]))

(5) -> (18), if ((x0[5] + -1 →^* x0[18]))

(5) -> (20), if ((x0[5] + -1 →^* x0[20]))

(6) -> (7), if ((x0[6] > 0 →^* TRUE)∧(x0[6] →^* x0[7]))

(7) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[7] →^* x0[0]))

(7) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[7] →^* x0[2]))

(8) -> (9), if ((x0[8] > 0 →^* TRUE)∧(x0[8] →^* x0[9]))

(9) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[9] →^* x0[0]))

(9) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[9] →^* x0[2]))

(10) -> (11), if ((x0[10] > 0 →^* TRUE)∧(x0[10] →^* x0[11]))

(11) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[11] →^* x0[0]))

(11) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[11] →^* x0[2]))

(12) -> (13), if ((x0[12] > 0 →^* TRUE)∧(x0[12] →^* x0[13]))

(13) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[13] →^* x0[0]))

(13) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[13] →^* x0[2]))

(14) -> (15), if ((x0[14] > 0 →^* TRUE)∧(x0[14] →^* x0[15]))

(15) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[15] →^* x0[0]))

(15) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[15] →^* x0[2]))

(16) -> (17), if ((x0[16] > 0 →^* TRUE)∧(x0[16] →^* x0[17]))

(17) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[17] →^* x0[0]))

(17) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[17] →^* x0[2]))

(18) -> (19), if ((x0[18] > 0 →^* TRUE)∧(x0[18] →^* x0[19]))

(19) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[19] →^* x0[0]))

(19) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[19] →^* x0[2]))

(20) -> (21), if ((x0[20] > 0 →^* TRUE)∧(x0[20] →^* x0[21]))

(21) -> (0), if ((11456_0_createNode_New →^* 1642_0_createNode_Return)∧(x0[21] →^* x0[0]))

(21) -> (2), if ((11456_0_createNode_New →^* 1963_0_createNode_Return)∧(x0[21] →^* x0[2]))

The set Q consists of the following terms:
11456_0_createNode_New
10199_0_createTree_LE(0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0)
1521_1_createNode_InvokeMethod

(34) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0) → COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0, 0), 1642_0_createNode_Return, x0) the following chains were created:

We consider the chain 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0]) → COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0]), COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1]) → 10199_0_CREATETREE_LE(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0])≥NonInfC∧11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0])≥COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])∧(U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0])≥NonInfC∧11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0])≥COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])∧(U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)

For Pair COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0) → 10199_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

We consider the chain COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1]) → 10199_0_CREATETREE_LE(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1])≥NonInfC∧COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1])≥10199_0_CREATETREE_LE(+(x0[1], -1))∧(U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧[1 + (-1)bso_54] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_54] ≥ 0)

For Pair 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0) → COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0, 0), 1963_0_createNode_Return, x0) the following chains were created:

We consider the chain 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2]) → COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2]), COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3]) → 10199_0_CREATETREE_LE(+(x0[3], -1)) which results in the following constraint:
(12)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3] ⇒ 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2])≥NonInfC∧11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2])≥COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])∧(U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥))

We simplified constraint (12) using rule (IV) which results in the following new constraint:
(13)    (>(x0[2], 0)=TRUE ⇒ 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2])≥NonInfC∧11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2])≥COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])∧(U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥))

We simplified constraint (13) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(14)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

We simplified constraint (14) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(15)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

We simplified constraint (15) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(16)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥)∧[(-1)bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(17)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥)∧[bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)

For Pair COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0) → 10199_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

We consider the chain COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3]) → 10199_0_CREATETREE_LE(+(x0[3], -1)) which results in the following constraint:
(18)    (COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3])≥NonInfC∧COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3])≥10199_0_CREATETREE_LE(+(x0[3], -1))∧(U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧[1 + (-1)bso_58] ≥ 0)

We simplified constraint (21) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(22)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧0 = 0∧[1 + (-1)bso_58] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[4]) → COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4]), COND_10199_0_CREATETREE_LE(TRUE, x0[5]) → 10199_0_CREATETREE_LE(+(x0[5], -1)) which results in the following constraint:
(23)    (>(x0[4], 0)=TRUE∧x0[4]=x0[5] ⇒ 10199_0_CREATETREE_LE(x0[4])≥NonInfC∧10199_0_CREATETREE_LE(x0[4])≥COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])∧(U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥))

We simplified constraint (23) using rule (IV) which results in the following new constraint:
(24)    (>(x0[4], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[4])≥NonInfC∧10199_0_CREATETREE_LE(x0[4])≥COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])∧(U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥))

We simplified constraint (24) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(25)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

We simplified constraint (25) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(26)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

We simplified constraint (26) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(27)    (x0[4] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(28)    (x0[4] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59 + (2)bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE(TRUE, x0) → 10199_0_CREATETREE_LE(+(x0, -1)) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE(TRUE, x0[5]) → 10199_0_CREATETREE_LE(+(x0[5], -1)) which results in the following constraint:
(29)    (COND_10199_0_CREATETREE_LE(TRUE, x0[5])≥NonInfC∧COND_10199_0_CREATETREE_LE(TRUE, x0[5])≥10199_0_CREATETREE_LE(+(x0[5], -1))∧(U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥))

We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(30)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(31)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(32)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧[1 + (-1)bso_62] ≥ 0)

We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(33)    ((U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧0 = 0∧[1 + (-1)bso_62] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE1(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[6]) → COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6]), COND_10199_0_CREATETREE_LE1(TRUE, x0[7]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7]) which results in the following constraint:
(34)    (>(x0[6], 0)=TRUE∧x0[6]=x0[7] ⇒ 10199_0_CREATETREE_LE(x0[6])≥NonInfC∧10199_0_CREATETREE_LE(x0[6])≥COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])∧(U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥))

We simplified constraint (34) using rule (IV) which results in the following new constraint:
(35)    (>(x0[6], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[6])≥NonInfC∧10199_0_CREATETREE_LE(x0[6])≥COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])∧(U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    (x0[6] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(39)    (x0[6] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63 + (2)bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE1(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE1(TRUE, x0[7]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7]) which results in the following constraint:
(40)    (COND_10199_0_CREATETREE_LE1(TRUE, x0[7])≥NonInfC∧COND_10199_0_CREATETREE_LE1(TRUE, x0[7])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥))

We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(41)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(42)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(43)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥)∧[(-1)bso_66] ≥ 0)

We simplified constraint (43) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(44)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥)∧0 = 0∧[(-1)bso_66] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE2(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[8]) → COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8]), COND_10199_0_CREATETREE_LE2(TRUE, x0[9]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9]) which results in the following constraint:
(45)    (>(x0[8], 0)=TRUE∧x0[8]=x0[9] ⇒ 10199_0_CREATETREE_LE(x0[8])≥NonInfC∧10199_0_CREATETREE_LE(x0[8])≥COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])∧(U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥))

We simplified constraint (45) using rule (IV) which results in the following new constraint:
(46)    (>(x0[8], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[8])≥NonInfC∧10199_0_CREATETREE_LE(x0[8])≥COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])∧(U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥))

We simplified constraint (46) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(47)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

We simplified constraint (47) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(48)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

We simplified constraint (48) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(49)    (x0[8] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

We simplified constraint (49) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(50)    (x0[8] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67 + (2)bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE2(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE2(TRUE, x0[9]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9]) which results in the following constraint:
(51)    (COND_10199_0_CREATETREE_LE2(TRUE, x0[9])≥NonInfC∧COND_10199_0_CREATETREE_LE2(TRUE, x0[9])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥))

We simplified constraint (51) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(52)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

We simplified constraint (52) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(53)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

We simplified constraint (53) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(54)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥)∧[1 + (-1)bso_70] ≥ 0)

We simplified constraint (54) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(55)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥)∧0 = 0∧[1 + (-1)bso_70] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE3(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[10]) → COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10]), COND_10199_0_CREATETREE_LE3(TRUE, x0[11]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11]) which results in the following constraint:
(56)    (>(x0[10], 0)=TRUE∧x0[10]=x0[11] ⇒ 10199_0_CREATETREE_LE(x0[10])≥NonInfC∧10199_0_CREATETREE_LE(x0[10])≥COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])∧(U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥))

We simplified constraint (56) using rule (IV) which results in the following new constraint:
(57)    (>(x0[10], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[10])≥NonInfC∧10199_0_CREATETREE_LE(x0[10])≥COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])∧(U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥))

We simplified constraint (57) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(58)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

We simplified constraint (58) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(59)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

We simplified constraint (59) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(60)    (x0[10] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

We simplified constraint (60) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(61)    (x0[10] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71 + (2)bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE3(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE3(TRUE, x0[11]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11]) which results in the following constraint:
(62)    (COND_10199_0_CREATETREE_LE3(TRUE, x0[11])≥NonInfC∧COND_10199_0_CREATETREE_LE3(TRUE, x0[11])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥))

We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥)∧[(-1)bso_74] ≥ 0)

We simplified constraint (65) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(66)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥)∧0 = 0∧[(-1)bso_74] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE4(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[12]) → COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12]), COND_10199_0_CREATETREE_LE4(TRUE, x0[13]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13]) which results in the following constraint:
(67)    (>(x0[12], 0)=TRUE∧x0[12]=x0[13] ⇒ 10199_0_CREATETREE_LE(x0[12])≥NonInfC∧10199_0_CREATETREE_LE(x0[12])≥COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])∧(U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥))

We simplified constraint (67) using rule (IV) which results in the following new constraint:
(68)    (>(x0[12], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[12])≥NonInfC∧10199_0_CREATETREE_LE(x0[12])≥COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])∧(U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥))

We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71)    (x0[12] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

We simplified constraint (71) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(72)    (x0[12] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75 + (2)bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE4(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE4(TRUE, x0[13]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13]) which results in the following constraint:
(73)    (COND_10199_0_CREATETREE_LE4(TRUE, x0[13])≥NonInfC∧COND_10199_0_CREATETREE_LE4(TRUE, x0[13])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥))

We simplified constraint (73) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(74)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

We simplified constraint (74) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(75)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

We simplified constraint (75) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(76)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥)∧[(-1)bso_78] ≥ 0)

We simplified constraint (76) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(77)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥)∧0 = 0∧[(-1)bso_78] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE5(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[14]) → COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14]), COND_10199_0_CREATETREE_LE5(TRUE, x0[15]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15]) which results in the following constraint:
(78)    (>(x0[14], 0)=TRUE∧x0[14]=x0[15] ⇒ 10199_0_CREATETREE_LE(x0[14])≥NonInfC∧10199_0_CREATETREE_LE(x0[14])≥COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])∧(U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥))

We simplified constraint (78) using rule (IV) which results in the following new constraint:
(79)    (>(x0[14], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[14])≥NonInfC∧10199_0_CREATETREE_LE(x0[14])≥COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])∧(U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥))

We simplified constraint (79) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(80)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

We simplified constraint (80) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(81)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

We simplified constraint (81) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(82)    (x0[14] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

We simplified constraint (82) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(83)    (x0[14] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79 + (2)bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE5(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE5(TRUE, x0[15]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15]) which results in the following constraint:
(84)    (COND_10199_0_CREATETREE_LE5(TRUE, x0[15])≥NonInfC∧COND_10199_0_CREATETREE_LE5(TRUE, x0[15])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥))

We simplified constraint (84) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(85)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

We simplified constraint (85) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(86)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

We simplified constraint (86) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(87)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥)∧[(-1)bso_82] ≥ 0)

We simplified constraint (87) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(88)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥)∧0 = 0∧[(-1)bso_82] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE6(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[16]) → COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16]), COND_10199_0_CREATETREE_LE6(TRUE, x0[17]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17]) which results in the following constraint:
(89)    (>(x0[16], 0)=TRUE∧x0[16]=x0[17] ⇒ 10199_0_CREATETREE_LE(x0[16])≥NonInfC∧10199_0_CREATETREE_LE(x0[16])≥COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])∧(U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥))

We simplified constraint (89) using rule (IV) which results in the following new constraint:
(90)    (>(x0[16], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[16])≥NonInfC∧10199_0_CREATETREE_LE(x0[16])≥COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])∧(U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥))

We simplified constraint (90) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(91)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

We simplified constraint (91) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(92)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

We simplified constraint (92) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(93)    (x0[16] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

We simplified constraint (93) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(94)    (x0[16] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83 + (2)bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE6(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE6(TRUE, x0[17]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17]) which results in the following constraint:
(95)    (COND_10199_0_CREATETREE_LE6(TRUE, x0[17])≥NonInfC∧COND_10199_0_CREATETREE_LE6(TRUE, x0[17])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥))

We simplified constraint (95) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(96)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

We simplified constraint (96) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(97)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

We simplified constraint (97) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(98)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥)∧[(-1)bso_86] ≥ 0)

We simplified constraint (98) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(99)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥)∧0 = 0∧[(-1)bso_86] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE7(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[18]) → COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18]), COND_10199_0_CREATETREE_LE7(TRUE, x0[19]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19]) which results in the following constraint:
(100)    (>(x0[18], 0)=TRUE∧x0[18]=x0[19] ⇒ 10199_0_CREATETREE_LE(x0[18])≥NonInfC∧10199_0_CREATETREE_LE(x0[18])≥COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])∧(U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥))

We simplified constraint (100) using rule (IV) which results in the following new constraint:
(101)    (>(x0[18], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[18])≥NonInfC∧10199_0_CREATETREE_LE(x0[18])≥COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])∧(U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥))

We simplified constraint (101) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(102)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (102) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(103)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (103) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(104)    (x0[18] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

We simplified constraint (104) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(105)    (x0[18] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87 + (2)bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE7(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE7(TRUE, x0[19]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19]) which results in the following constraint:
(106)    (COND_10199_0_CREATETREE_LE7(TRUE, x0[19])≥NonInfC∧COND_10199_0_CREATETREE_LE7(TRUE, x0[19])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥))

We simplified constraint (106) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(107)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

We simplified constraint (107) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(108)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

We simplified constraint (108) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(109)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥)∧[1 + (-1)bso_90] ≥ 0)

We simplified constraint (109) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(110)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥)∧0 = 0∧[1 + (-1)bso_90] ≥ 0)

For Pair 10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE8(>(x0, 0), x0) the following chains were created:

We consider the chain 10199_0_CREATETREE_LE(x0[20]) → COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20]), COND_10199_0_CREATETREE_LE8(TRUE, x0[21]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21]) which results in the following constraint:
(111)    (>(x0[20], 0)=TRUE∧x0[20]=x0[21] ⇒ 10199_0_CREATETREE_LE(x0[20])≥NonInfC∧10199_0_CREATETREE_LE(x0[20])≥COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])∧(U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥))

We simplified constraint (111) using rule (IV) which results in the following new constraint:
(112)    (>(x0[20], 0)=TRUE ⇒ 10199_0_CREATETREE_LE(x0[20])≥NonInfC∧10199_0_CREATETREE_LE(x0[20])≥COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])∧(U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥))

We simplified constraint (112) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(113)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

We simplified constraint (113) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(114)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

We simplified constraint (114) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(115)    (x0[20] + [-1] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

We simplified constraint (115) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(116)    (x0[20] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91 + (2)bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)

For Pair COND_10199_0_CREATETREE_LE8(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0) the following chains were created:

We consider the chain COND_10199_0_CREATETREE_LE8(TRUE, x0[21]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21]) which results in the following constraint:
(117)    (COND_10199_0_CREATETREE_LE8(TRUE, x0[21])≥NonInfC∧COND_10199_0_CREATETREE_LE8(TRUE, x0[21])≥11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])∧(U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥))

We simplified constraint (117) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(118)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

We simplified constraint (118) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(119)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

We simplified constraint (119) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(120)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥)∧[(-1)bso_94] ≥ 0)

We simplified constraint (120) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(121)    ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥)∧0 = 0∧[(-1)bso_94] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0) → COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0, 0), 1642_0_createNode_Return, x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x0[0] ≥ 0∧[(-1)bso_52] ≥ 0)
COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0) → 10199_0_CREATETREE_LE(+(x0, -1))
- ((U^Increasing(10199_0_CREATETREE_LE(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_54] ≥ 0)
11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0) → COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0, 0), 1963_0_createNode_Return, x0)
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])), ≥)∧[bni_55 + (-1)Bound*bni_55] + [(2)bni_55]x0[2] ≥ 0∧[(-1)bso_56] ≥ 0)
COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0) → 10199_0_CREATETREE_LE(+(x0, -1))
- ((U^Increasing(10199_0_CREATETREE_LE(+(x0[3], -1))), ≥)∧0 = 0∧[1 + (-1)bso_58] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE(>(x0, 0), x0)
- (x0[4] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])), ≥)∧[(-1)Bound*bni_59 + (2)bni_59] + [(2)bni_59]x0[4] ≥ 0∧[1 + (-1)bso_60] ≥ 0)
COND_10199_0_CREATETREE_LE(TRUE, x0) → 10199_0_CREATETREE_LE(+(x0, -1))
- ((U^Increasing(10199_0_CREATETREE_LE(+(x0[5], -1))), ≥)∧0 = 0∧[1 + (-1)bso_62] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE1(>(x0, 0), x0)
- (x0[6] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])), ≥)∧[(-1)Bound*bni_63 + (2)bni_63] + [(2)bni_63]x0[6] ≥ 0∧[1 + (-1)bso_64] ≥ 0)
COND_10199_0_CREATETREE_LE1(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])), ≥)∧0 = 0∧[(-1)bso_66] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE2(>(x0, 0), x0)
- (x0[8] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])), ≥)∧[(-1)Bound*bni_67 + (2)bni_67] + [(2)bni_67]x0[8] ≥ 0∧[(-1)bso_68] ≥ 0)
COND_10199_0_CREATETREE_LE2(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])), ≥)∧0 = 0∧[1 + (-1)bso_70] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE3(>(x0, 0), x0)
- (x0[10] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])), ≥)∧[(-1)Bound*bni_71 + (2)bni_71] + [(2)bni_71]x0[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)
COND_10199_0_CREATETREE_LE3(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])), ≥)∧0 = 0∧[(-1)bso_74] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE4(>(x0, 0), x0)
- (x0[12] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])), ≥)∧[(-1)Bound*bni_75 + (2)bni_75] + [(2)bni_75]x0[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)
COND_10199_0_CREATETREE_LE4(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])), ≥)∧0 = 0∧[(-1)bso_78] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE5(>(x0, 0), x0)
- (x0[14] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])), ≥)∧[(-1)Bound*bni_79 + (2)bni_79] + [(2)bni_79]x0[14] ≥ 0∧[1 + (-1)bso_80] ≥ 0)
COND_10199_0_CREATETREE_LE5(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])), ≥)∧0 = 0∧[(-1)bso_82] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE6(>(x0, 0), x0)
- (x0[16] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])), ≥)∧[(-1)Bound*bni_83 + (2)bni_83] + [(2)bni_83]x0[16] ≥ 0∧[1 + (-1)bso_84] ≥ 0)
COND_10199_0_CREATETREE_LE6(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])), ≥)∧0 = 0∧[(-1)bso_86] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE7(>(x0, 0), x0)
- (x0[18] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])), ≥)∧[(-1)Bound*bni_87 + (2)bni_87] + [(2)bni_87]x0[18] ≥ 0∧[(-1)bso_88] ≥ 0)
COND_10199_0_CREATETREE_LE7(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])), ≥)∧0 = 0∧[1 + (-1)bso_90] ≥ 0)
10199_0_CREATETREE_LE(x0) → COND_10199_0_CREATETREE_LE8(>(x0, 0), x0)
- (x0[20] ≥ 0 ⇒ (U^Increasing(COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])), ≥)∧[(-1)Bound*bni_91 + (2)bni_91] + [(2)bni_91]x0[20] ≥ 0∧[1 + (-1)bso_92] ≥ 0)
COND_10199_0_CREATETREE_LE8(TRUE, x0) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0)
- ((U^Increasing(11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])), ≥)∧0 = 0∧[(-1)bso_94] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(11456_0_createNode_New) = [-1]
POL(13058_0_createNode_InvokeMethod) = [-1]
POL(12798_0_createNode_InvokeMethod) = [-1]
POL(12951_0_createNode_InvokeMethod) = [-1]
POL(12836_0_createNode_InvokeMethod) = [-1]
POL(10199_0_createTree_LE(x₁)) = [-1]
POL(0) = 0
POL(10224_0_createTree_Return) = [-1]
POL(1521_1_createNode_InvokeMethod) = [-1]
POL(11456_1_createTree_InvokeMethod(x₁, x₂)) = [-1]
POL(2056_0_createNode_InvokeMethod) = [-1]
POL(11724_0_createTree_InvokeMethod(x₁)) = [-1]
POL(2088_0_createNode_InvokeMethod) = [-1]
POL(11275_0_createTree_InvokeMethod(x₁)) = [-1]
POL(11584_0_createTree_InvokeMethod(x₁)) = [-1]
POL(11354_0_createTree_InvokeMethod(x₁)) = [-1]
POL(13204_0_createTree_InvokeMethod(x₁)) = [-1]
POL(12923_0_createTree_InvokeMethod(x₁)) = [-1]
POL(13109_0_createTree_InvokeMethod(x₁)) = [-1]
POL(12976_0_createTree_InvokeMethod(x₁)) = [-1]
POL(1642_0_createNode_Return) = [-1]
POL(1963_0_createNode_Return) = [-1]
POL(11456_1_CREATETREE_INVOKEMETHOD(x₁, x₂)) = [-1] + [2]x₂
POL(COND_11456_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃)) = [-1] + [2]x₃
POL(>(x₁, x₂)) = [-1]
POL(10199_0_CREATETREE_LE(x₁)) = [2]x₁
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(COND_11456_1_CREATETREE_INVOKEMETHOD1(x₁, x₂, x₃)) = [-1] + [2]x₃
POL(COND_10199_0_CREATETREE_LE(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE1(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE2(x₁, x₂)) = [2]x₂
POL(COND_10199_0_CREATETREE_LE3(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE4(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE5(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE6(x₁, x₂)) = [-1] + [2]x₂
POL(COND_10199_0_CREATETREE_LE7(x₁, x₂)) = [2]x₂
POL(COND_10199_0_CREATETREE_LE8(x₁, x₂)) = [-1] + [2]x₂

The following pairs are in P_>:

COND_11456_1_CREATETREE_INVOKEMETHOD(TRUE, 1642_0_createNode_Return, x0[1]) → 10199_0_CREATETREE_LE(+(x0[1], -1))
COND_11456_1_CREATETREE_INVOKEMETHOD1(TRUE, 1963_0_createNode_Return, x0[3]) → 10199_0_CREATETREE_LE(+(x0[3], -1))
10199_0_CREATETREE_LE(x0[4]) → COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])
COND_10199_0_CREATETREE_LE(TRUE, x0[5]) → 10199_0_CREATETREE_LE(+(x0[5], -1))
10199_0_CREATETREE_LE(x0[6]) → COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])
COND_10199_0_CREATETREE_LE2(TRUE, x0[9]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[9])
10199_0_CREATETREE_LE(x0[10]) → COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])
10199_0_CREATETREE_LE(x0[12]) → COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])
10199_0_CREATETREE_LE(x0[14]) → COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])
10199_0_CREATETREE_LE(x0[16]) → COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])
COND_10199_0_CREATETREE_LE7(TRUE, x0[19]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[19])
10199_0_CREATETREE_LE(x0[20]) → COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])

The following pairs are in P_bound:

11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0]) → COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])
11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2]) → COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])
10199_0_CREATETREE_LE(x0[4]) → COND_10199_0_CREATETREE_LE(>(x0[4], 0), x0[4])
10199_0_CREATETREE_LE(x0[6]) → COND_10199_0_CREATETREE_LE1(>(x0[6], 0), x0[6])
10199_0_CREATETREE_LE(x0[8]) → COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])
10199_0_CREATETREE_LE(x0[10]) → COND_10199_0_CREATETREE_LE3(>(x0[10], 0), x0[10])
10199_0_CREATETREE_LE(x0[12]) → COND_10199_0_CREATETREE_LE4(>(x0[12], 0), x0[12])
10199_0_CREATETREE_LE(x0[14]) → COND_10199_0_CREATETREE_LE5(>(x0[14], 0), x0[14])
10199_0_CREATETREE_LE(x0[16]) → COND_10199_0_CREATETREE_LE6(>(x0[16], 0), x0[16])
10199_0_CREATETREE_LE(x0[18]) → COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])
10199_0_CREATETREE_LE(x0[20]) → COND_10199_0_CREATETREE_LE8(>(x0[20], 0), x0[20])

The following pairs are in P_≥:

11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0]) → COND_11456_1_CREATETREE_INVOKEMETHOD(>(x0[0], 0), 1642_0_createNode_Return, x0[0])
11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2]) → COND_11456_1_CREATETREE_INVOKEMETHOD1(>(x0[2], 0), 1963_0_createNode_Return, x0[2])
COND_10199_0_CREATETREE_LE1(TRUE, x0[7]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])
10199_0_CREATETREE_LE(x0[8]) → COND_10199_0_CREATETREE_LE2(>(x0[8], 0), x0[8])
COND_10199_0_CREATETREE_LE3(TRUE, x0[11]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])
COND_10199_0_CREATETREE_LE4(TRUE, x0[13]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])
COND_10199_0_CREATETREE_LE5(TRUE, x0[15]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])
COND_10199_0_CREATETREE_LE6(TRUE, x0[17]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])
10199_0_CREATETREE_LE(x0[18]) → COND_10199_0_CREATETREE_LE7(>(x0[18], 0), x0[18])
COND_10199_0_CREATETREE_LE8(TRUE, x0[21]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])

There are no usable rules.

(35) Complex Obligation (AND)

(36) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
11456_0_createNode_New → 13058_0_createNode_InvokeMethod
11456_0_createNode_New → 12798_0_createNode_InvokeMethod
11456_0_createNode_New → 12951_0_createNode_InvokeMethod
11456_0_createNode_New → 12836_0_createNode_InvokeMethod
10199_0_createTree_LE(0) → 10224_0_createTree_Return
11456_0_createNode_New → 1521_1_createNode_InvokeMethod
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11724_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11724_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11275_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11275_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11584_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11584_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2056_0_createNode_InvokeMethod, x0) → 11354_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 11354_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 13204_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 12923_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 13109_0_createTree_InvokeMethod(x0)
11456_1_createTree_InvokeMethod(2088_0_createNode_InvokeMethod, x0) → 12976_0_createTree_InvokeMethod(x0)
1521_1_createNode_InvokeMethod → 1642_0_createNode_Return
1521_1_createNode_InvokeMethod → 2056_0_createNode_InvokeMethod
1521_1_createNode_InvokeMethod → 2088_0_createNode_InvokeMethod
1521_1_createNode_InvokeMethod → 1963_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 11456_1_CREATETREE_INVOKEMETHOD(1642_0_createNode_Return, x0[0]) → COND_11456_1_CREATETREE_INVOKEMETHOD(x0[0] > 0, 1642_0_createNode_Return, x0[0])
(2): 11456_1_CREATETREE_INVOKEMETHOD(1963_0_createNode_Return, x0[2]) → COND_11456_1_CREATETREE_INVOKEMETHOD1(x0[2] > 0, 1963_0_createNode_Return, x0[2])
(7): COND_10199_0_CREATETREE_LE1(TRUE, x0[7]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[7])
(8): 10199_0_CREATETREE_LE(x0[8]) → COND_10199_0_CREATETREE_LE2(x0[8] > 0, x0[8])
(11): COND_10199_0_CREATETREE_LE3(TRUE, x0[11]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[11])
(13): COND_10199_0_CREATETREE_LE4(TRUE, x0[13]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[13])
(15): COND_10199_0_CREATETREE_LE5(TRUE, x0[15]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[15])
(17): COND_10199_0_CREATETREE_LE6(TRUE, x0[17]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[17])
(18): 10199_0_CREATETREE_LE(x0[18]) → COND_10199_0_CREATETREE_LE7(x0[18] > 0, x0[18])
(21): COND_10199_0_CREATETREE_LE8(TRUE, x0[21]) → 11456_1_CREATETREE_INVOKEMETHOD(11456_0_createNode_New, x0[21])